This file was created with JabRef 2.2.
Encoding: Cp1252

@STRING{entcs = {ENTCS}}

@STRING{fmsd = {Form.\@ Method.\@ Syst.\@ Des.\@}}

@STRING{ic = {Inf.\@ Comput.\@}}

@STRING{ijfcs = {Int.\@ J.\@ Found.\@ Comput.\@ Sci.\@}}

@STRING{ipl = {Inform.\@ Process.\@ Lett.\@}}

@STRING{jacm = {J.\@ ACM}}

@STRING{jcss = {J.\@ Comput.\@ Syst.\@ Sci.\@}}

@STRING{lncs = {LNCS}}

@STRING{lnm = {Lect.\@ Notes Math.\@}}

@STRING{mst = {Math.\@ Syst.\@ Theory}}

@STRING{sicomp = {SIAM J.\@ Comput.\@}}

@STRING{sttt = {Int.\@ J.\@ Softw.\@ Tools Technol.\@ Transf.\@}}

@STRING{tams = {Trans.\@ Amer.\@ Math.\@ Soc.\@}}

@STRING{tcs = {Theoret.\@ Comput.\@ Sci.\@}}}

@STRING{tcsys = {Theory Comput.\@ Syst.\@}}

@STRING{tocl = {ACM Trans.\@ Comput.\@ Log.\@}}





@ARTICLE{Kupferman2001,
  author = {O. Kupferman and M. Vardi},
  title = {Weak alternating automata are not that weak},
  journal = tocl,
  year = {2001},
  volume = {2},
  number = {3}
}

@INPROCEEDINGS{Emerson1991,
  author = {E. Emerson and C. Jutla},
  title = {Tree Automata, Mu-Calculus and Determinacy (Extended Abstract)},
  booktitle = {Proc. of FOCS'91},
  year = {1991},
}


@INPROCEEDINGS{Dax2008,
  author = {C. Dax and F. Klaedtke},
  title = {Alternation Elimination by Complementation},
  booktitle = {Proc. of LPAR '08},
  year = {2008},
  volume = ?,
  series = lncs,
}
















@INPROCEEDINGS{Banieqbal1987,
  author = {B. Banieqbal and H. Barringer},
  title = {Temporal Logic with Fixed Points},
  booktitle = {Proc. of Temporal Logic in Specification '87},
  year = {1989},
  volume = 298,
  series = lncs,
}

@ARTICLE{Bloem2007,
  author = {R. Bloem and A. Cimatti and I. Pill and M. Roveri},
  title = {Symbolic Implementation of Alternating Automata},
  journal = ijfcs,
  year = {2007},
  volume = {18},
  number = {4}
}

@ARTICLE{Boigelot2005,
  author = {B. Boigelot and S. Jodogne and P. Wolper},
  title = {An Effective Decision Procedure for Linear Arithmetic over the Integers
	and Reals},
  journal = tocl,
  year = {2005},
  volume = {6},
  number = {3}
}

@TECHREPORT{Bustan2005,
  author = {D. Bustan and D. Fisman and J. Havlicek},
  title = {Automata Construction for {PSL}},
  institution = {Computer Science and Applied Mathematics, 
                 The Weizmann Institute of Science, Israel},
  year = {2005},
}

@INCOLLECTION{Chang1991,
  author = {E. Chang and Z. Manna and A. Pnueli},
  title = {The Safety-Progress Classification},
  booktitle = {Logic and Algebra of Specifications},
  publisher = {Springer},
  year = {1993},
  series = {NATO ASI Series}
}

@INPROCEEDINGS{Dax2007,
  author = {C. Dax and J. Eisinger and F. Klaedtke},
  title = {Mechanizing the Powerset Construction for Restricted Classes of $\omega$-Automata},
  booktitle = {Proc. of ATVA'07},
  year = {2007},
  volume = 4762,
  series = lncs,
}

@INPROCEEDINGS{Dax2006,
  author = {C. Dax and M. Hofmann and M. Lange},
  title = {A Proof System for the Linear Time $\mu$-Calculus},
  booktitle = {Proc. of FSTTCS'06},
  year = {2006},
  volume = 4437,
  series = lncs,
}

@ARTICLE{Dax2005,
  author = {C. Dax and M. Lange},
  title = {Game Over: The Foci Approach to {LTL} Satisfiability and Model Checking},
  journal = entcs,
  year = {2005},
  volume = {119},
}


@INPROCEEDINGS{Gastin2003,
  author = {P. Gastin and D. Oddoux},
  title = {{LTL} with Past and Two-Way Very-Weak Alternating Automata},
  booktitle = {Proc. of MFCS'03},
  year = {2003},
  volume = 2747,
  series = lncs,
}

@INPROCEEDINGS{Gastin2001,
  author = {P. Gastin and D. Oddoux},
  title = {Fast {LTL} to {B{\"u}chi} Automata Translation},
  booktitle = {Proc. of CAV'01},
  year = {2001},
  volume = 2102,
  series = lncs,
}

@ARTICLE{Jutla1997,
  author = {C. Jutla},
  title = {Determinization and Memoryless Winning Strategies},
  journal = ic,
  year = {1997},
  volume = {133},
  number = {2}
}

@INPROCEEDINGS{Klarlund1991,
  author = {N. Klarlund},
  title = {Progress Measures for Complementation of omega-Automata with Applications
	to Temporal Logic},
  booktitle = {Proc. of FOCS'01},
  year = {1991},
}

@inproceedings{Kupferman2005,
  author    = {O. Kupferman and M. Vardi},
  title     = {Complementation Constructions for Nondeterministic Automata on Infinite Words},
  booktitle = {Proc. of TACAS'05},
  year      = 2005,
  volume    = 3440,
  series    = lncs,
}

@INPROCEEDINGS{Kupferman2006,
  author = {O. Kupferman and R. Lampert},
  title = {On the construction of fine automata for safety properties},
  booktitle = {Proc. of ATVA'07},
  year = {2006},
  volume = 4218,
  series = lncs,
}


@ARTICLE{Kupferman2001b,
  author = {O. Kupferman and M. Vardi},
  title = {Model checking of safety properties},
  journal = fmsd,
  year = {2001},
  volume = {19},
  number = {3}
}

@INPROCEEDINGS{Lange2001,
  author = {M. Lange and C. Stirling},
  title = {Focus Games for Satisfiability and Completeness of Temporal Logic},
  booktitle = {Proc. of LICS'01},
  year = {2001}
}

@MASTERSTHESIS{Loeding1998,
  author = {C. L{\"o}ding},
  title = {Methods for the transformation of omega-automata: Complexity and
	connection to second order logic},
  school = {University of Kiel, Germany},
  year = {1998}
}

@ARTICLE{Miyano1984,
  author = {S. Miyano and T. Hayashi},
  title = {Alternating finite automata on {$\omega$}-words},
  journal = tcs,
  year = {1984},
  volume = {32},
  number = {3}
}


@Article{Muller1995,
  author = 	 {D. Muller and P. Schupp},
  title = 	 {Simulating alternating tree automata by nondeterministic 
                  automata: New results and new proofs of the theorems of 
                  {Rabin}, {McNaughton} and {Safra}},
  journal = 	 tcs,
  year = 	 {1995},
  volume = 	 {141},
}

@ARTICLE{Muller1992,
  author = {D. Muller and A. Saoudi and P. Schupp},
  title = {Alternating automata, the weak monadic theory of trees and its complexity},
  journal = tcs,
  year = {1992},
  volume = {97},
  number = {2},
}

@ARTICLE{Muller1987,
  author = {D. Muller and P. Schupp},
  title = {Alternating Automata on Infinite Trees},
  journal = tcs,
  year = {1987},
  volume = {54},
}

@ARTICLE{Piterman2003,
  author = {N. Piterman and M. Vardi},
  title = {From bidirectionality to alternation},
  journal = tcs,
  year = {2003},
  volume = {1--3},
}

@inproceedings{Kupferman2001c,
  author    = {Orna Kupferman and Nir Piterman and Moshe Vardi},
  title     = {Extended Temporal Logic Revisited},
  booktitle = {Proc. of CONCUR'01},
  year      = 2001,
  volume    = 2154,
  series    = lncs,
}



@INPROCEEDINGS{Pnueli1977,
  author = {A. Pnueli},
  title = {The temporal logic of programs},
  booktitle = {Proc. of FOCS'77},
  year = {1977}
}

@INPROCEEDINGS{Safra1988,
  author = {S. Safra},
  title = {On the Complexity of omega-Automata},
  booktitle = {Proc. of FOCS'88},
  year = {1988},
}

@inproceedings{Vardi2007a,
  author    = {M. Vardi},
  title     = {Automata-Theoretic Model Checking Revisited},
  booktitle = {Proc. of VMCAI'07},
  year      = {2007},
  volume    = {4349},
  series    = lncs,
}

@INPROCEEDINGS{Vardi2007,
  author = {M. Vardi},
  title = {The {B{\"u}chi} Complementation Saga},
  booktitle = {Proc. of STACS'07},
  year = {2007},
  volume = {4393},
  series = lncs,
}

@ARTICLE{Vardi1989,
  author = {M. Vardi},
  title = {A Note on the Reduction of Two-Way Automata to One-Way Automata},
  journal = ipl,
  year = {1989},
  volume = {30},
  number = {5},
}

@INPROCEEDINGS{Vardi1988,
  author = {M. Vardi},
  title = {A Temporal Fixpoint Calculus},
  booktitle = {Proc. of POPL'88},
  year = {1988}
}

@inproceedings{Vardi1998,
  author    = {M. Vardi},
  title     = {Reasoning about The Past with Two-Way Automata},
  booktitle = {Proc. of ICALP'98},
  year      = {1998}, 
  volume    = {1443},
  series    = lncs,
}

@PROCEEDINGS{Thomas2001,
  title = {Automata, Logics, and Infinite Games: A Guide to Current Research},
  year = {2002},
  editor = {E. Gr{\"a}del and W. Thomas and T. Wilke},
  volume = {2500},
  series = lncs,
  booktitle = {Automata, Logics, and Infinite Games}
}

@MISC{Psl2005,
  title = {{IEEE} Standard for Property Specification Language ({PSL})},
  howpublished = {IEEE Std 1850TM},
  year = 2005,
  month = {Oct.},
}

@InProceedings{Gerth1995,
  author = 	 {R. Gerth and D. Peled and M. Vardi and P. Wolper},
  title = 	 {Simple on-the-fly automatic verification of
                  linear temporal logic},
  booktitle =    {Proc. of PSTV'95},
  year = 	 {1996},
  volume = 	 {38},
  series = 	 {IFIP Conf. Proc.},
}


@article{Fritz2005,
  author    = {C. Fritz and T. Wilke},
  title     = {Simulation relations for alternating {B{\"u}chi} automata},
  journal   = tcs,
  volume    = {338},
  number    = {1--3},
  year      = {2005},
}


@article{Etessami2005,
  author    = {K. Etessami and T. Wilke and R. Schuller},
  title     = {Fair Simulation Relations, Parity Games, and State
                  Space Reduction for {B\"uchi} Automata},
  journal   = sicomp,
  volume    = {34},
  number    = {5},
  year      = {2005},
}


@phdthesis{Rohde1979,
 author = {G. Rohde},
 title = {Alternating automata and the temporal logic of ordinals},
 year = {1997},
 isbn = {0-591-63604-2},
 school = {University of Illinois at Urbana-Champaign},
 address = {Champaign, IL, USA},
}

@inproceedings{Loeding2000,
  author    = {C. L{\"o}ding and W. Thomas},
  title     = {Alternating Automata and Logics over Infinite Words},
  booktitle = {IFIP TCS},
  year      = {2000},
  pages     = {521-535},
}